package minsat;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

/**
 * This class contains static methods that invoke the MinSatz algorithm or the optimal solver on
 * a MinSat instance.
 */
public class MinSatz
{
  /**
   * Implementation of Algorithm 1 from the paper, finds a set of bindings that yields a minimum
   * satisfied weight of soft clauses while still satisfying all hard clauses
   * 
   * @param formula
   *          Clauses eligible for satisfaction
   * @param lowerBound
   *          Current lower bound for satisfied weight and bindings that yield that bound
   * @param newBinding
   *          The binding that needs to be added to the set of bindings during this iteration
   * @return Bindings for all variables and the weight of the optimal solution
   */
  public static BindingsAndBound runMinSatz(Formula formula, BindingsAndBound lowerBound,
                                            Binding newBinding)
  {
    // create new copy of bindings to attempt to propagate the new binding
    BindingsAndBound newLowerBound = new BindingsAndBound(lowerBound);

    // hard unit propagation on formula
    try {
      formula.propagate(newBinding, newLowerBound, false);
    }
    catch (IllegalEmptyClauseException e) {
      // if hard clause violated, return previous bound
      return lowerBound;
    }

    double softFalsifiedWeight = formula.empty();

    // if formula is empty or only has empty clauses, return bindings + max of empty weight or LB
    if (formula.isEmpty()) {
      if (lowerBound.bound > softFalsifiedWeight) // we can't beat the previous best
        return lowerBound;
      else {
        newLowerBound.bound = softFalsifiedWeight;
        return newLowerBound;
      }
    }

    // set UB to empty weight + overestimate(formula)
    double upperBound = softFalsifiedWeight + formula.overestimate();

    // if upper bound < lower bound, a better solution cannot be found from this path
    if (upperBound <= lowerBound.bound) return lowerBound;

    // select a literal x from formula
    final Literal x = formula.select();

    // LB = runMinSat(formula, bound + x=true)
    BindingsAndBound boundTrue =
        runMinSatz(new Formula(formula), newLowerBound, new Binding(x, true));

    // LB = runMinSat(formula, bound + x=false)
    BindingsAndBound boundFalse =
        runMinSatz(new Formula(formula), newLowerBound, new Binding(x, false));

    return (boundTrue.bound > boundFalse.bound) ? boundTrue : boundFalse;
  }

  /**
   * Uses a brute force O(2^n) algorithm to find the optimal MinSat solution
   * 
   * @param formula
   *          Formula to solve
   * @return Mapping from literal name to optimal binding
   */
  public static Map<String, Boolean> optimalSat(Formula formula)
  {
    Map<String, Boolean> bestBindings = new HashMap<String, Boolean>();
    double bestWeight = Double.NEGATIVE_INFINITY;

    // find all unique literals
    Set<Literal> uniqueLiterals = new HashSet<Literal>();
    for (Clause c : formula.getClauses()) {
      for (Literal literal : c.literals) {
        uniqueLiterals.add(literal.nonNegated());
      }
    }

    int possibileAssignments = (int) Math.pow(2, uniqueLiterals.size());
    List<Literal> literalList = new ArrayList<Literal>(uniqueLiterals);
    Map<String, Boolean> currentBindings;
    int listSize = literalList.size();
    int[] preCalculatedPowers = new int[listSize];
    double weight;
    for (int i = 0; i < listSize; i++)
      preCalculatedPowers[i] = (int) Math.pow(2, i);

    // iterate over all possibilities: O(2^n)
    for (int i = 0; i < possibileAssignments; i++) {
      currentBindings = new HashMap<String, Boolean>();
      for (int j = 0; j < listSize; j++) {
        currentBindings.put(literalList.get(j).name, ((i & preCalculatedPowers[j]) == 0) ? false
            : true);
      }
      // evaluate binding
      weight = new Formula(formula).evaluate(currentBindings);

      if (weight > bestWeight) {
        bestWeight = weight;
        bestBindings = new HashMap<String, Boolean>(currentBindings);
      }
    }

    return bestBindings;
  }

  /**
   * Converts a BindingsAndBound object into a map from literal names to bindings, used for data
   * output
   * 
   * @param bindings
   *          Bindings to be converted
   * @return Map from names to bindings
   */
  public static Map<String, Boolean> convertToMap(BindingsAndBound bindings)
  {
    Map<String, Boolean> result = new HashMap<String, Boolean>();

    for (Binding b : bindings.bindings) {
      result.put(b.literal.name, ((b.literal.neg) ? !b.binding : b.binding));
    }
    return result;
  }
}
